Skip to content

Fix #1099: KColoring to Satisfiability - #1108

Open
isPANN wants to merge 4 commits into
1075-growth-domainfrom
issue-1099
Open

Fix #1099: KColoring to Satisfiability#1108
isPANN wants to merge 4 commits into
1075-growth-domainfrom
issue-1099

Conversation

@isPANN

@isPANN isPANN commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator

Summary

Add a direct, witness-preserving CNF encoding from runtime K-Coloring on simple graphs to Satisfiability.

Fixes #1099

@codecov

codecov Bot commented Aug 2, 2026 •
edited
Loading

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 97.67198% with 111 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.94%. Comparing base (cb54ea0) to head (cc67770).

Files with missing lines Patch % Lines
src/rules/graph.rs 94.81% 29 Missing ⚠️
src/unit_tests/growth.rs 96.01% 25 Missing ⚠️
src/unit_tests/rules/pareto.rs 98.22% 22 Missing ⚠️
src/growth.rs 98.22% 11 Missing ⚠️
src/solvers/registry.rs 95.73% 9 Missing ⚠️
src/solvers/ilp/solver.rs 86.20% 4 Missing ⚠️
src/rules/pareto.rs 97.95% 3 Missing ⚠️
src/unit_tests/solvers/brute_force.rs 83.33% 3 Missing ⚠️
src/unit_tests/solvers/registry.rs 98.70% 3 Missing ⚠️
src/solvers/resolver.rs 98.71% 1 Missing ⚠️
... and 1 more
Additional details and impacted files 
@@            Coverage Diff             @@
##             main    #1108      +/-   ##
==========================================
- Coverage   98.00%   97.94%   -0.07%     
==========================================
  Files        1044     1053       +9     
  Lines      107366   110791    +3425     
==========================================
+ Hits       105228   108513    +3285     
- Misses       2138     2278     +140

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@isPANN

isPANN commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator Author

Implementation Summary

Changes

  • Added a direct KColoring<KN, SimpleGraph> to Satisfiability reduction using one-hot assignment variables, pairwise exactly-one clauses, and edge-conflict clauses.
  • Added exact reduction overhead metadata, witness extraction, and the canonical five-cycle example.
  • Added ten focused tests covering the closed loop, clause structure and sizes, extraction, feasible and infeasible cycles, zero-color cases, disconnected and isolated vertices, self-loops, parallel edges, and more colors than vertices.
  • Added the fixture-driven paper theorem and tutorial plus the SAT 2024 primary-source citation.
  • Regenerated and verified graph, schema, and canonical-example exports; ignored generated outputs were not committed.

Verification

  • Mathematical constructor: 739,171 checks, 0 failures.
  • Independent adversary: 52,533 checks, 0 failures.
  • Cross-comparison: 8,605 instances, 0 disagreements.
  • Full workspace tests, documentation tests, paper build, formatting, and clippy all passed.

Deviations from Plan

  • None.

Open Questions

  • None.

@isPANN
isPANN changed the base branch from main to 1075-growth-domain August 2, 2026 05:48
@isPANN

isPANN commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator Author

Agentic Review Report

Review base: a9067297 (1075-growth-domain)

Structural Check

Structural Review: rule KColoring → Satisfiability

Structural Completeness

# Check Status
1 Rule file exists PASS — src/rules/kcoloring_satisfiability.rs
2 #[reduction(...)] macro present PASS — src/rules/kcoloring_satisfiability.rs:39
3 ReductionResult impl present PASS — src/rules/kcoloring_satisfiability.rs:18
4 ReduceTo impl present PASS — src/rules/kcoloring_satisfiability.rs:46
5 Test link present PASS — src/rules/kcoloring_satisfiability.rs:110
6 Test file exists PASS — src/unit_tests/rules/kcoloring_satisfiability.rs
7 Closed-loop test present PASS — src/unit_tests/rules/kcoloring_satisfiability.rs:11
8 Registered in rules/mod.rs PASS — module at src/rules/mod.rs:56; example aggregation at src/rules/mod.rs:468
9 Canonical rule example registered PASS — C5/k=3 fixture and source/target witnesses at src/rules/kcoloring_satisfiability.rs:91
10 Example-db lookup tests exist PASS — generic lookup/build and authored-direct-reduction coverage; full consistency suite passed
11 Paper reduction-rule entry PASS — docs/paper/reductions.typ:12200
12 Blacklisted generated files absent PASS — none appears in the corrected five-file diff

Build Status

  • make test: PASS — 5,441 library tests, 75 integration tests, 330 CLI tests, 17 pred_sym tests, 26 macro tests, and all doctests passed
  • make clippy: PASS — all targets with ilp-highs, warnings denied

Semantic Review

  • PR scope: OK — against a9067297, exactly five task-specific files and 374 insertions.
  • Reduction construction: OK — the variable map and ALO, AMO, and edge-conflict clauses exactly match the issue.
  • Mathematical trace: OK — the two-vertex, one-edge, three-color trace produces the expected six variables, two ALO clauses, six AMO clauses, and three edge-conflict clauses.
  • extract_solution: OK — partitions the assignment into vertex blocks and returns the unique true color.
  • Overhead accuracy: OK — nk variables, n+n*k*(k-1)/2+mk clauses, and nk+n*k*(k-1)+2mk literals match construction and paper.
  • Canonical example: OK — C5/k=3 witness and 15-bit assignment match; C5/k=2 infeasibility is tested.
  • Edge cases: OK — empty/k=0, nonempty/k=0, loops, parallel edges, disconnected/isolated vertices, and k>n are covered.
  • Paper proof and literature: OK — both correctness directions, extraction, exact counts, domain extensions, and SAT 2024 citation are sound.
  • Primitive registration: OK — exactly one primitive endpoint implementation exists.

Issue Compliance

# Check Status
1 Source/target match OK
2 Reduction algorithm matches OK
3 Solution extraction matches OK
4 Correctness preserved OK
5 Overhead expressions match OK
6 Example matches OK

Summary

  • 12/12 structural checks passed
  • 6/6 issue-compliance checks passed
  • No structural or semantic issues found

Quality Check

Quality Review

Design Principles

  • DRY: OK — variable indexing is centralized and encoding/extraction logic is not duplicated.
  • KISS: OK — the three CNF clause families use direct loops without unnecessary abstractions.
  • HC/LC: OK — construction, extraction, example, registration, documentation, and tests remain in their appropriate modules.

HCI

  • Not applicable — no CLI or MCP files changed in the corrected review range.

Test Quality

  • Naive test detection: OK
    • Nontrivial five-vertex closed loop verifies extracted witnesses.
    • Exact variable, clause, literal, and clause-family assertions independently pin down the encoding.
    • Feasible and infeasible odd-cycle cases test both directions.
    • Boundary/adversarial coverage includes zero colors, empty/disconnected graphs, loops, parallel edges, and excess colors.
    • Extraction is checked against a concrete satisfying assignment.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

None.

Minor (Nice to Have)

None.

Summary

  • No quality issues found.
  • The five-file change is focused, direct, cohesive, and supported by substantive semantic and edge-case tests.

Agentic Feature Tests

Feature: KColoring/SimpleGraph/KN → Satisfiability
Mode: Blind documentation review followed by verification against PR head cc67770a
Verdict: Pass
Critical issues: 0

Documentation Surface

  • README.md
  • docs/src/cli.md

The documented catalog workflow makes the direct rule discoverable without source inspection.

Verification Results

Check Command Result
Catalog registration pred list | rg 'KColoring|Satisfiability' PASS — source and target variants listed
Source details/rule discovery pred show KColoring PASS — direct Satisfiability edge and overhead displayed
Target details pred show Satisfiability PASS — fields and incoming KColoring edge displayed
Canonical source creation pred create --example KColoring/SimpleGraph/KN --to Satisfiability PASS — canonical C5/k=3 created
Source solve pred solve kcoloring.json --solver brute-force PASS — Or(true), coloring [0,1,0,1,2]
Direct reduction pred reduce kcoloring.json --to Satisfiability PASS — one-step path, 15 variables, 35 clauses
Bundle solve/extraction pred solve kcoloring-to-sat.json --solver brute-force PASS — extracted [2,1,2,1,0]
Extracted witness evaluation pred evaluate kcoloring.json --config 2,1,2,1,0 PASS — Or(true)

Findings

No functional, discoverability-blocking, or documentation-blocking issues were found. The direct rule is discoverable, creates the expected target, solves through the bundle, and extracts a valid coloring. No tracked files were modified.

Generated by review-pipeline

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

[Rule] KColoring to Satisfiability

1 participant

@isPANN